tg-me.com/sqlhub/1867
Last Update:
🚀Масштабная архитектура на базе, которая содержит 671 млрд параметров, что в 96 раз больше, чем у предыдущей версии Prover-V1.5 (7 млрд).
Построен на базе архитектуры «смеси экспертов» (MoE), что снижает затраты на обучение и повышает эффективность решения задач.
Модель заточена на формальное доказательство теорем с помощью языка программирования Lean 4, обеспечивая 100% логическую точность.
Lean 4 — это зависимо типизированный функциональный язык программирования и интерактивное средство доказательства теорем.
Результаты:
• Новая Sota( 88,9%) на MiniF2F-test.
• DeepSeek-Prover-V2 смогла доказать 49 теорем из 658.
Для тренировки использовались 8 млн синтетических примеров, созданных через рекурсивный поиск решений теорем.
🔍 Как это работает:
1) Разложение теорем: DeepSeek-V3 по prompt'у разбивает сложные задачи на подцели.
2) Формализация: Пошаговые рассуждения переводятся в доказательства на Lean 4.
3) Cold-start: Полученные цепочки рассуждений и формальные доказательства используются как начальные данные для обучения модели.
• 7 B — базовый вариант.
• 671 B — расширенная версия на базе DeepSeek-V3-Base.
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
